COMMENT ⊗   VALID 00006 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	\magnification = \magstephalf
C00004 00003
C00007 00004	\vfill\eject
C00011 00005	\vfill\eject
C00015 00006	\vfill\eject\end
C00020 ENDMK
C⊗;
\magnification = \magstephalf
\catcode`|=13
\def|#1|{\hbox{\it#1\/}}
\parindent 0pt
\parskip 0pt
\def\pskip{\penalty-1000\vskip 6pt plus 2pt minus 1pt}
\def\ppskip{\penalty-2000\vskip 10pt plus 3pt minus 2pt}
\def\no(#1){\noindent\hbox to 6em{(#1)\hfill}}
\catcode`⊗=13
\def⊗{\hbox to 2em{}}
\def\IF{\mathop{\hbox{\bf if}}}
\def\THEN{\mathrel{\bf then}}
\def\ELSE{\mathrel{\bf else}}
\def\AND{\mathrel{\bf and}}
\def\OR{\mathrel{\bf or}}
\def\NOT{\mathop{\hbox{\bf not}}}
\def\N{\mathop{\hbox{\bf n}}}
\def\T{\hbox{\tt T}}
\def\F{\hbox{\tt F}}
\def\NIL{\hbox{\tt NIL}}
\def\.{\mathbin{.}}
\def\A{\mathop{\hbox{\bf a}}}
\def\D{\mathop{\hbox{\bf d}}}
\def\AD{\mathop{\hbox{\bf ad}}}
\def\DD{\mathop{\hbox{\bf dd}}}
\def\ADD{\mathop{\hbox{\bf add}}}
\def\ADDD{\mathop{\hbox{\bf addd}}}
\def\EQ{\mathrel{\bf eq}}
\def\AT{\mathop{\hbox{\bf at}}}
\def\quote#1{\hbox{\sfcode`.=1000\tt#1}}
\def\list#1{\langle#1\rangle}
\def\xskip{\hskip7pt plus3pt minus4pt}

\centerline{CS 206---Recursive Programming and Proving}
\vskip 20pt
\centerline {Midterm Exam Solutions}
\centerline{Thursday, November 10, 1983}

\ppskip
\no(1)$|odds1|\,u←$\par
$⊗⊗⊗⊗\IF\N u\THEN\NIL$\par
$⊗⊗⊗⊗\ELSE\A u\.|evens1|\,\D u$\par

\pskip
$⊗⊗⊗|evens1|\,u←$\par
$⊗⊗⊗⊗\IF\N u\THEN\NIL$\par
$⊗⊗⊗⊗\ELSE |odds1|\,\D u$\par
\pskip

$⊗⊗⊗|combine1|[u,v]←$\par
$⊗⊗⊗⊗\IF\N u\THEN v$\par
$⊗⊗⊗⊗\ELSE\A u\.|combine1|[v,\D u]$\par
\pskip
Another way of defining these functions is:\par
\pskip

$⊗⊗⊗|odds|\,u←$\par
$⊗⊗⊗⊗\IF\N u\OR\N\D u\THEN u$\par
$⊗⊗⊗⊗\ELSE\A u\.|odds|\,\DD u$\par
\pskip
$⊗⊗⊗|evens|\,u←$\par
$⊗⊗⊗⊗\IF\N u\OR\N\D u\THEN \NIL$\par
$⊗⊗⊗⊗\ELSE\AD u\.|evens|\,\DD u$\par
\pskip
$⊗⊗⊗|combine|[u,v]←$\par
$⊗⊗⊗⊗\IF\N u\THEN v$\par
$⊗⊗⊗⊗\ELSE\IF\N v\THEN u$\par
$⊗⊗⊗⊗\ELSE\A u\.\A v\.|combine|[\D u,\D v]$\par
\pskip
Any combination of the above definitions (one for each function) works fine,
although they seemed to appear mainly as either the first set or the second.
The second set was more common, whereas the first is easier to prove things 
about. 

\ppskip
\ppskip
\no(2)$|ifsimp|[u]←$\par
$⊗⊗⊗⊗\IF\AT u\THEN u$\par
$⊗⊗⊗⊗\ELSE\IF \A u = {\tt IF}\THEN $\par
$⊗⊗⊗⊗⊗⊗\IF |ifstep|[u]=u\THEN u\ELSE |ifsimp|\,[|ifstep|[u]]$\par
$⊗⊗⊗⊗\ELSE u$\par
\pskip

$⊗⊗⊗|ifstep|[u]←$\par
$⊗⊗⊗⊗\IF\AD u = \T\THEN|ifsimp|[\ADD u]$\par
$⊗⊗⊗⊗\ELSE\IF\AD u = \F\THEN|ifsimp|[\ADDD u]$\par
$⊗⊗⊗⊗\ELSE\langle{\tt IF}\,\,\,\,|ifsimp|[\AD u]\,\,\,\,
			|ifsimp|[|replace|[\AD u, \T,\ADD u]]$\par
$⊗⊗⊗⊗⊗⊗⊗⊗⊗|ifsimp|[|replace|[\AD u,\F,\ADDD u]]\rangle $\par
\pskip

$⊗⊗⊗|replace|[x,y,z]←$\par
$⊗⊗⊗⊗\IF z=x \THEN y$\par
$⊗⊗⊗⊗\ELSE\IF\AT z\THEN z$\par
$⊗⊗⊗⊗\ELSE |replace|[x,y,\A z]\.|replace|[x,y,\D z]$\par

\pskip
\vfill\eject

\no(3) The function $|subst|$ is defined by:\par
$⊗⊗⊗|subst|[x,y,z]←$\par$⊗⊗⊗⊗⊗\IF\AT z\THEN [\IF z=y\THEN x\ELSE z]$\par
$⊗⊗⊗⊗⊗\ELSE|subst|[x,y,\A z]\.|subst|[x,y,\D z]$,\par
\noindent we prove 
$$∀x\, y\, z.\,\AT y ⊃ |subst|[x,y,|subst|[x,y,z]] = |subst|[|subst|[x,y,x],y,z]$$
by S-expression induction on z. We use the schema
$$(∀z.\,\AT z⊃\Phi(z))∧(∀z.\,¬\AT z∧\Phi(\A z)∧\Phi(\D z)⊃\Phi(z))⊃∀z.\,\Phi(z).$$
where $\Phi(z)=
|subst|[x,y,|subst|[x,y,z]] = |subst|[|subst|[x,y,x],y,z]$. We
make no assumptions about $x$ and assume that $y$ is an atom. This will allow 
us to conclude $∀x\, y\, z.\,\AT y ⊃ \Phi(z)$ from $∀z\.\,\Phi(z)$.
\pskip
The atomic case ($\AT z$):\par
(i) $z=y$:\par
$⊗⊗⊗|subst|[x,y,|subst|[x,y,z]]=|subst|[x,y,[\IF\AT z\THEN[\IF z=y\THEN x\ELSE
z]]]$\par
$⊗⊗⊗⊗=|subst|[x,y,[\IF\T\THEN[\IF\T\THEN x\ldots]]]$\par
$⊗⊗⊗⊗=|subst|[x,y,x]$\par
$⊗⊗⊗|subst|[|subst|x,y,x],y,z]=\IF\AT z\THEN[\IF z=y\THEN |subst|[x,y,x]\ELSE z]
\ELSE\ldots$\par
$⊗⊗⊗⊗=|subst|[x,y,x]$\par
\pskip\noindent (ii) $z≠y$:\par
$⊗⊗⊗|subst|[x,y,|subst|[x,y,z]]=|subst|[x,y,[\IF\AT z\THEN[\IF z=y\THEN x\ELSE
z]\ELSE\ldots]]$\par
$⊗⊗⊗⊗=|subst|[x,y,[\IF\T\THEN[\IF\F\THEN \ldots\ELSE z]\ELSE\ldots]]$\par
$⊗⊗⊗⊗=|subst|[[x,y,z]$\par\pskip
$⊗⊗⊗|subst|[|subst|[x,y,x],y,z]=\IF\AT z\THEN[\IF z=y\THEN \ldots\ELSE z]\ELSE
\ldots$
\par$⊗⊗⊗⊗=|subst|[x,y,z]$\par
\pskip
The non-atomic case ($¬\AT z$):\par
We assume by induction that $\Phi(\A z)$ and $\Phi(\D z)$ are true, i.e.\par
$⊗⊗|subst|[x,y,|subst|[x,y,\A z]] = |subst|[|subst|[x,y,x],y,\A z]$, and\par
$⊗⊗|subst|[x,y,|subst|[x,y,\D z]] = |subst|[|subst|[x,y,x],y,\D z]$.\par
\pskip
$⊗⊗⊗|subst|[x,y,|subst|[x,y,z]]$\par
$⊗⊗⊗⊗=|subst|[x,y,[\IF\AT z\THEN\ldots\ELSE
|subst|[x,y,\A z].|subst|[x,y,\D z]]$\par
$⊗⊗⊗⊗=\IF\F\THEN\ldots\ELSE
|subst|[x,y,|subst|[x,y,\A z]]\.|subst|[x,y,|subst|[x,y,\D z]]$\par
$⊗⊗⊗⊗=|subst|[x,y,|subst|[x,y,\A z]]\.|subst|[x,y,|subst|[x,y,\D z]]$\par
$⊗⊗⊗⊗=|subst|[|subst|[x,y,x],y,\A z]\.|subst|[|subst|[x,y,x],y,\D z]$, by the 
ind. hypothesis.\par
$⊗⊗⊗⊗=\IF\F\THEN\ldots$\par
$⊗⊗⊗⊗\,\,\,\,\,\ELSE
|subst|[|subst|[x,y,x],y,\A z]\.|subst|[|subst|[x,y,x],y,\D z]$, by $\IF$ rules.
\par $⊗⊗⊗⊗=\IF\AT z\THEN\ldots\ELSE
|subst|[|subst|[x,y,x],y,\A z]\.|subst|[|subst|[x,y,x],y,\D z]$\par
$⊗⊗⊗⊗=|subst|[|subst|[x,y,x],y,z]$, by the definition of $|subst|$, and we are
done.


\vfill\eject
\ppskip
\no(4) The proof of $∀u.\,|combine|[|odds|\,u,|evens|\,u]=u$ varies according
to the definition you use. When $|combine|$ is defined as in $|combine1|$,
the proof especially simple and elegant. We present two proofs:\hfill\par
$∀u\.\,|combine1|[|odds1|\,u,|evens1|\,u]=u$ by List induction, and\par
$∀u\.\,|combine|[|odds|\,u,|evens|\,u]=u$ by Rank induction.\par
The List induction proof uses the schema
$$\Phi(\NIL)∧(∀x\, u.\,\Phi(u)⊃\Phi(x\.u))⊃∀u.\,\Phi(u).$$

The $\NIL$ case is\par
$⊗⊗|combine1|[|odds1|\,\NIL,|evens1|\,\NIL]=|combine|[\NIL,\NIL]=\NIL$\par
The interesting part, therefore, is the inductive step. We assume $\Phi(u)$, 
and attempt to prove $\Phi(x\.u)$.

Using the first set of definitions:\par
$⊗⊗|combine1|[|odds1|\,x\.u,|evens1|\,x\.u]=|combine1|[x\.|evens1|\,u,|odds1|\,u]$\par
$⊗⊗⊗=\IF\N [x\.|evens1|\,u]\THEN\ldots\ELSE x\.|combine1|[|odds1|\,u,|evens1|\,u]
=x\.u$ by the inductive hypothesis.
\pskip
We now come to our Rank induction proof, for the second set of definitions.
We take the function $|length|\,$ as our rank function. 
$$|length|\,u←\,\IF\N u\THEN 0\ELSE 1 + |length|\,\D u$$
We therefore use the induction schema :
$$[∀u.\,[∀v.\, |length|\,v < |length|\,u ⊃ \Phi(v)]⊃\Phi(u)]⊃∀u.\,\Phi(u)$$
The cases $|length|\,u = 0$ ($u=\NIL$) and $|length|\,u=1$ need seperate treatments:
\par The case $u=\NIL$ is identical to the $\NIL$ case in the first proof.
The case $|length|\,u=1$ ($u=x\.\NIL$) goes as follows:\par
$⊗⊗|combine|[|odds|\,x\.\NIL,|evens|\,x\.\NIL]=|combine|[x\.\NIL,\NIL]$\par
$⊗⊗⊗=\IF\N x\.\NIL\THEN\ldots\ELSE\IF\N\NIL\THEN x\.\NIL\ELSE\ldots$\par
$⊗⊗⊗=x\.\NIL$\par

Finally, the induction step; assume $|length|\,u ≥ 2$, in particular $¬\N\D u$.
Further assume by induction that for all lists $v$ of lesser $|length|\,$, 
$\Phi(v)$ holds, where $\Phi$ is as in the first proof.\par
$⊗⊗|combine|[|odds|\,u,|evens|\,u]=|combine|[\A u\.|odds|\,\DD u, \AD u\.|evens|\,\DD u
]$\par
$⊗⊗⊗=\A u\.\AD u\.|combine|[|odds|\,\DD u,|evens|\,\DD u]$, and by the induction
hypothesis\par
$⊗⊗⊗=\A u\.\AD u\.\DD u =\A u\.\D u= u$\par
$\DD u$ is lower in $|length|\,$ rank than $u$, therefore $\Phi(\DD u)$ holds
by our induction hypothesis, so $|combine|[|odds|\,\DD u,|evens|\,\DD u]=\DD u$.
This completes the proof.
\vfill\eject\end
****************************

$⊗⊗⊗|member|[x,u]←\NOT\N u\AND[[x=\A u]\OR|member|[x,\D u]].$\par
\pskip
The proof in part (b) is by list induction on the formula $\Phi(u)$:
$|member|[x,|remove|[x,u]]=\NIL$.  The proof will not make any assumptions
about $x$, so a $∀x$ quantifier may be added at the end.  Either form of
the list induction principle may be used.  First let us use
$$\Phi(\NIL)∧(∀u.\,¬\N u∧\Phi(\D u)⊃\Phi(u))⊃∀u.\,\Phi(u).$$
We can see that
$\Phi(\NIL)$ is true because $|remove|[x,\NIL]=\NIL$ by the definition of
|remove|; thus
\pskip
$⊗⊗⊗|member|[x,|remove|[x,\NIL]]=|member|[x,\NIL]$\par
$⊗⊗⊗⊗=\NIL,$\par
\pskip
by expanding the definition of |member|.  Now, 
using the assumptions $¬\N u$ and $\Phi(\D u)$, which is
$|member|[x,|remove|[x,\D u]]=\NIL$, we compute $|member|[x,|remove|[x,u]]$
by first expanding the |remove| and simplifying:
\pskip
$⊗⊗⊗|member|[x,|remove|[x,u]]$\par
$⊗⊗⊗⊗=\IF x=\A u\THEN|member|[x,|remove|[x,\D u]]$\par
$⊗⊗⊗⊗⊗\ELSE|member|[x,\A u\.|remove|[x,\D u]]$\par
\pskip
Now we use the inductive hypothesis to replace $|member|[x,|remove|[x,\D u]]$
by \NIL, and expand the oter use of |member|:
\pskip
$⊗⊗⊗⊗=\IF x=\A u\THEN\NIL\ELSE [x=\A u]\OR|member|[x,|remove|[x,\D u]]$\par
$⊗⊗⊗⊗=\NIL.$\par
\pskip
The second occurrence of $x=\A u$ in the line above can be replaced by \NIL,
since it occurs in a context where $x=\A u$ is known to be false.
\pskip
The other form of the list induction principle is
$$\Phi(\NIL)∧(∀y\,u.\,\Phi(u)⊃\Phi(y\.u))⊃∀u.\,\Phi(u).$$
The variable $y$ is used instead of the usual $x$ because $x$ is already in
use as the first argument to |remove| and |member|.  The proof of
$\Phi(\NIL)$ is the
same as before, and using the assumption $\Phi(u)$, we have
\pskip
$⊗⊗⊗|member|[x,|remove|[x,y\.u]$\par
$⊗⊗⊗⊗=\IF x=y\THEN|member|[x,|remove|[x,u]]$\par
$⊗⊗⊗⊗⊗\ELSE|member|[x,y\.|remove|[x,u]]$\par
$⊗⊗⊗⊗=\IF x=y\THEN\NIL\ELSE [x=y]\OR|member|[x,|remove|[x,u]]$\par
$⊗⊗⊗⊗=\NIL,$
\pskip
using the same steps as in the previous version of the proof.

\ppskip
\no(3)$g[n]←\IF n≥0\AND |odd|[n]\THEN 0\ELSE\bot,$\par
$⊗⊗⊗h[n]←\IF n≥0\THEN 0\ELSE\bot.$\par
\pskip
Of the six statements in part (b), only (iii) and (v) are true.  The
functions $f$ and $g$ each are defined for values at which the other is


\ppskip
\no(4)$|simplify|\,|spexp|←$\par
$⊗⊗⊗⊗\IF\AT|spexp|\THEN|spexp|$\par
$⊗⊗⊗⊗\ELSE\IF\A|spexp|=\quote{PLUS}\THEN$\par
$⊗⊗⊗⊗⊗[λu.\,\IF\N u\THEN 0\ELSE\IF\N\D u\THEN\A u\ELSE\quote{PLUS}\.u]
	[|simplus|\,\D|spexp|]$\par
$⊗⊗⊗⊗\ELSE\IF\A|spexp|=\quote{TIMES}\THEN$\par
$⊗⊗⊗⊗⊗[λu.\,\IF u=0\THEN 0$\par
$⊗⊗⊗⊗⊗⊗\ELSE\IF\N u\THEN 1$\par
$⊗⊗⊗⊗⊗⊗\ELSE\IF\N\D u\THEN\A u$\par
$⊗⊗⊗⊗⊗⊗\ELSE\quote{TIMES}\.u][|simtimes|\,\D|spexp|]$\par
\pskip
$⊗⊗⊗|simplus|\,u←$\par
$⊗⊗⊗⊗\IF\N u\THEN\NIL$\par
$⊗⊗⊗⊗\ELSE[λe.\,\IF e=0\THEN|simplus|\,\D u\ELSE e\.|simplus|\,\D u]
	\,[|simplify|\,\A u]$\par
\pskip
$⊗⊗⊗|simtimes|\,u←$\par
$⊗⊗⊗⊗\IF\N u\THEN\NIL$\par
$⊗⊗⊗⊗\ELSE[λe.\,\IF e=0\THEN 0$\par
$⊗⊗⊗⊗⊗⊗\ELSE\IF e=1\THEN|simtimes|\,\D u$\par
$⊗⊗⊗⊗⊗⊗\ELSE[λv.\,\IF v=0\THEN 0\ELSE e\.v][|simtimes|\,\D u]]
	\,[|simplify|\,\A u]$\par

\vfill\end